﻿{-
This is a naive implementation of unification algorithm. It is the 2nd
assignment of course algorithm
Author: Zhou Liang
Stu No: 1100379020
-}

-- Define the module where we are
module Unification where

-- Type Definition
type Constant = String
type Variable = String
type Function = String
data Term = Const Constant | Var Variable | Func Function [Term] deriving Show
data Substitute = Substitute Variable Term deriving Show

-- include function
-- if a terms includes a variable, return true, else false
include :: Variable -> Term -> Bool
include var (Func func ((Var inner_var) : terms)) = if var == inner_var then True else include var (Func func terms)
include var (Func func ((Const _) : terms)) = include var (Func func terms)
include var (Func func ((Func inner_fun inner_terms) : terms)) = if include var (Func inner_fun inner_terms) then True else include var (Func func terms)
include _ _ = False

-- combineResult function
-- combine two substitions, return true if they can be merged
combineResult :: (Bool, [Substitute]) -> (Bool, [Substitute]) -> (Bool, [Substitute])
combineResult (bool1, subs1) (bool2, subs2) = if bool1 && bool2 then (True, subs1 ++ subs2) else (False, [])

-- substitute function
-- apply the substitutions to term, return the term
substitute :: [Substitute] -> Term -> Term
substitute [] term = term
substitute [_] (Const const) = (Const const)
substitute ((Substitute sub_var sub_term) : subs) (Var var) = if var == sub_var then sub_term else substitute subs (Var var)
substitute subs (Func func terms) = Func func (map (substitute subs) terms)
    
-- A naive implementation of unification algorithm

unify :: Term -> Term -> (Bool, [Substitute])
unify (Const const1) (Const const2) = if const1 == const2 then (True, []) else (False, [])
unify (Var var1) (Var var2) = if var1 == var2 then (True, []) else (True, [Substitute var1 (Var var2)])
unify (Var var) term = if include var term then (False, []) else (True, [Substitute var term])
unify term (Var var) = if include var term then (False, []) else (True, [Substitute var term])
unify (Func func1 terms1) (Func func2 terms2) = if (func1 /= func2) || (length terms1 /= length terms2) then (False, []) else
    foldl (\ (bool, subs) (term1, term2) -> combineResult (bool, subs) (unify (substitute subs term1) (substitute subs term2))) (True, []) (zip terms1 terms2)
unifier _ _ = (False, [])


-- Test Terms
term1 = Func "f" [Var "x"]
term2 = Func "g" [Const "a"]
term3 = Func "f" [Const "b"]
term4 = Func "f" [Var "x", Func "g" [Var "x"]]
term5 = Func "f" [Var "y", Func "g" [Var "y"]]
term6 = Func "f" [Var "x1", Var "x2", Func "g" [Var "x3"]]
term7 = Func "f" [Var "y1", Func "h" [Var "y2", Const "a"], Var "y3"]

-- Print Help Info
help = do
			putStrLn "You can unify two terms by unify term1 term2"
			putStrLn "Or you can enter the function mannually: unify (Func \"f\" [Var \"x\"]) (Func \"f\" [Const \"b\"])"
			putStrLn "Here are test terms already defined"
			putStrLn "term1: f(x)"
			putStrLn "term2: g(a)"
			putStrLn "term3: f(b)"
			putStrLn "term4: f(x, g(x))"
			putStrLn "term5: f(y, g(y))"
			putStrLn "term6: f(x1, x2, g(x3))"
			putStrLn "term7: f(y1, h(y2, a), y3)"
